D realizes2 es.P(es) == w:World, p:FairFifo. PossibleWorld(D;w)  P(ES(w)) 

latex

---

clarification:

d-realizes2{i:l}
d-realizes2(D; es.P(es))
== w:world{i:l}, p:fair-fifo{i:l}(w). possible-world{i:l}(D; w)  P(w-es{i:l}(w; p)) 

latex

Definitions	World, x:A. B(x), FairFifo, P  Q, PossibleWorld(D;w), ES(the_w)
FDL editor aliases	d-realizes2